Inference at * 
Iof proof for Lemma can-apply-compose:


  A, B, C:Type, g:(A(B + Top)), f:(B(C + Top)), x:A.
  (can-apply(f o g  ;x))  {(can-apply(g;x)) & (can-apply(f;do-apply(g;x)))} 

latex

 by ((Auto) 
CollapseTHEN (MoveToConcl (-1))) 
CollapseTHEN (((RWO "can-apply-compose-sq" (0))

CollapseTHENA (Auto)) 
CollapseTHEN ((Unfold `guard` ( 0)) 
CollapseTHEN (AutoBoolCase 
Ccan-apply(g;x)))) 

latex

C.

Definitions	can-apply(f;x), Type, {T}, Unit, P  Q, x:A  B(x), , s = t, b, A, , True, b, suptype(S; T), left + right, do-apply(f;x), S  T, x:A. B(x), x:AB(x), Top, x:A.B(x), Void, P  Q, P & Q, t  T, False
Lemmas	can-apply-compose-sq, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, bool wf, assert wf, can-apply wf, do-apply wf, false wf